\documentclass[xcolor=dvipsnames,mathserif,svgnames,11pt]{beamer}

% for a handout:
%
%\documentclass[handout,11pt]{beamer}
%
%\usepackage{pgfpages}
%\pgfpagesuselayout{2 on 1}[letterpaper,border shrink=5mm]
\usepackage{stmaryrd}
\usepackage{savesym}
\usepackage{amssymb} 

\usepackage{amsmath, amsthm}
\usepackage{listings}
\usepackage{proof}
\lstdefinelanguage{MyHaskell}
{alsoletter={+,|,->, =, ::}, morekeywords={+,|,->, =, ::, data, Int, max, case, of}
}


\lstdefinelanguage{MyLambda}
{alsoletter={\., |, ->, = }, morekeywords={=,|, -> ,\., lam , fix, case, of}}


%\lstset{language=MyHaskell, keywordstyle=\color{scyan},basicstyle=\ttfamily}

\definecolor{syellow}{RGB}{181,137,0}
\definecolor{scyan}{RGB}{42,161,152}

\DefineNamedColor{named}{MyBlue}{RGB}{38,139,210}
\DefineNamedColor{named}{Base3}{RGB}{253,246,227}
\DefineNamedColor{named}{Base00}{RGB}{101,123,131}

\newcommand{\ep}[0]{\epsilon} 
\newcommand{\yemph}[1]{\colorbox{yellow}{#1}}
\newcommand{\cemph}[1]{\textcolor{Blue}{#1}}
\newcommand{\remph}[1]{\textcolor{Red}{#1}}
\newcommand{\uemph}[1]{\underline{#1}}
\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 
\newcommand{\ind}[0]{\mathsf{Ind}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\rec}[0]{\mathsf{rec}} 
\newcommand{\case}[0]{\mathsf{case}} 
\newcommand{\eq}[0]{\mathsf{Eq}} 
\newcommand{\add}[0]{\mathsf{add}} 
\newcommand{\cc}[0]{\mathbf{CC}} 
\makeatletter
\newsavebox{\@brx}
\newcommand{\llangle}[1][]{\savebox{\@brx}{\(\m@th{#1\langle}\)}%
  \mathopen{\copy\@brx\kern-0.6\wd\@brx\usebox{\@brx}}}
\newcommand{\rrangle}[1][]{\savebox{\@brx}{\(\m@th{#1\rangle}\)}%
  \mathclose{\copy\@brx\kern-0.6\wd\@brx\usebox{\@brx}}}
\makeatother

\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 
\newcommand{\intern}[1]{\llbracket #1 \rrbracket^{-1}} 

%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} |--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}

\include{seppp_annotated}
\mode<presentation>
{
  %\usetheme{Warsaw}
  % or ...
%gets rid of bottom navigation bars
%\setbeamertemplate{footline}[page number]{}

%gets rid of navigation symbols
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\usetheme{default}
%\usecolortheme[named=MyBlue]{structure}
%\setbeamercolor{background canvas}{bg=Base3}
%\setbeamercolor{normal text}{fg=Base00}

%\usetheme{Edinburgh}

%  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.

\title[Mini-Sym]
{From Self Type to System $\mathfrak{G}$ through Comprehension }

\author{Peng Fu}

\institute[University of Iowa]
{  
  Dept. of Computer Science\\
  University of Iowa}
\date{\today}
%\date{May 22, 2013 }
% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}



% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
%\AtBeginSubsection[]
%{
%  \begin{frame}<beamer>
%    \frametitle{Outline}
%    \tableofcontents[currentsection,currentsubsection]
%  \end{frame}
%}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}

\begin{document}

\begin{frame}[plain]
  \titlepage
\end{frame}

\begin{frame}
  \frametitle{Background}
  \begin{itemize}
    \item Self type generalization and instantiation.

      \
      
      \begin{tabular}{ll}
      \infer{\Gamma \vdash t : \iota x.T}{\Gamma \vdash t: [t/x]T}
      
      &
      
      \infer{\Gamma \vdash t: [t/x]T}{\Gamma \vdash t : \iota x.T}
        
      \end{tabular}
      \item Mutually Recursive definitions. 
      \item Scott encoding.  
      \item Church encoding.
        \item $\Pi x:\nat. x + 0 = x$.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Motivations}
  \begin{itemize}
    \item Church encoding $\Leftrightarrow$ Consistent system.
      \item Scott encoding $\Leftrightarrow$ Inconsistent system. 

      \item Understanding self type $\iota x.T$.
%%   \item Its relation to polymorphic dependent type theory.
      \item Reason about general programs. 
  \end{itemize}
\end{frame}

%% \begin{frame}[fragile]
%% \frametitle{Church Encoding}

%% \begin{itemize}

%% \item Church numerals

%% $\mathsf{Zero}\ := \lambda s.\lambda z.z$

%%   $\mathsf{One}\ := \lambda s.\lambda z.\yemph{s}\ z$
  
%%   $\mathsf{Two}\ := \lambda s.\lambda z.\cemph{s\ s}\ z$

%% \item Numeric Functions

%% $\mathsf{Succ}\ := \lambda n. \lambda s.\lambda z.s\ (n\ s\ z)$

%% $\mathsf{add}\ := \lambda n.\lambda m. n\ \mathsf{Succ}\ m$

%% $\mathsf{pred}\ := \lambda n. \lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f)) (\lambda u.x)\ (\lambda u.u)$
  
%% \end{itemize}
%% \end{frame}

\begin{frame}[fragile]
\frametitle{Self Type Mechanism as Comprehension}

\begin{itemize}
\item<1-> Instantiation and Generalization.
  
  \
  
  \begin{tabular}{l}
  \infer={\Gamma \vdash t : [t/x]T}{\Gamma \vdash t:\iota x.T}    
  \end{tabular}

  
  \item<2-> Comprehension axiom.
    
    $t \ep \{x | F\} \Leftrightarrow [t/x]F$
    
    \item<3-> How about this?   
      
      \
  
      \begin{tabular}{l}
      \infer={\Gamma \vdash t \ep [t/x]T}{\Gamma \vdash t \ep \iota x.T}        
      \end{tabular}
      
      \item<4-> Now this.
        
        \

        \begin{tabular}{l}
        \infer={\Gamma \vdash [t/x]T}{\Gamma \vdash t \ep \iota x.T}          
        \end{tabular}

        
\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{System $\mathfrak{G}$}
\begin{itemize}
\item Syntax

  Lambda Term $t ::= \ x\ | \ \lambda x.t \ | \ t t'$

  Set $S ::= X^1 \ | \ \iota x.F$ 

  Formula $F ::= X^0 \ | \ t \ep S \ | \ \forall x.F \ | \ F \to F' \ | \ \Pi X^0.F \ | \ \Pi X^1.F$
 

 
 Context $\Gamma ::= \cdot \ | \ F, \Gamma$
   \item Axioms 
     
     Beta-equivalence $(\lambda x.t)t' =_{\beta} [t'/x]t$
     
     Comprehension $t\ep (\iota x.F) =_{\iota} [t/x]F$

\end{itemize}

\end{frame}

\begin{frame}
  \frametitle{System $\mathfrak{G}$: Logical Rules}

  \footnotesize{
\begin{tabular}{ll}
    
\infer[\textit{Var}]{\Gamma \vdash F}{F \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash F_2}{\Gamma \vdash 
F_1 &  F_1 =_{\beta, \iota} F_2}

\\
\\
\infer[\textit{Forall}]{\Gamma \vdash  \forall x.F}
{\Gamma \vdash F &  x \notin \mathrm{FV}(\Gamma)}

&
\infer[\textit{Instantiate}]{\Gamma \vdash [t'/x]F}{\Gamma
\vdash \forall x.F}
\\
\\
\infer[\textit{Pi}]{\Gamma \vdash  \Pi X^i.F}
{\Gamma \vdash F & X^i \notin \mathrm{FV}(\Gamma) & i= 0,1}

&
\infer[\textit{Inst0}]{\Gamma \vdash [F'/X^0]F}{\Gamma \vdash \Pi X^0.F}

\\
\\

\infer[\textit{Imp}]{\Gamma \vdash  F_1\to F_2}
{\Gamma, F_1 \vdash F_2}

&

\infer[\textit{MP}]{\Gamma \vdash F_2}{\Gamma
\vdash F_1 \to F_2 & \Gamma \vdash  F_1}
\\
\\

\infer[\textit{Inst1}]{\Gamma \vdash [S/X^1]F}{\Gamma \vdash  \Pi X^1.F}

\end{tabular}
}
  
\end{frame}

\begin{frame}
  \frametitle{A Polymorphic Dependent Type System}

   Internal Types \yemph{$U\ := X^1 \ | \ \iota x.Q \ | \ \Pi x:U.U' \ | \ \Delta X^1.U$}

   Internal Formula $Q \ := X^0 \ | \ t \ep U \ | \ \Pi X^0.Q \ | \ Q \to Q' \ | \ \forall x.Q \ | \  \Pi X^1. Q$

  Internal Context $\Psi\ :=  \ \cdot \ | \ \Psi, t\ep U$

  \
  
  \footnotesize{
  \begin{tabular}{ll}
%%\infer[toSet]{\intern{\Gamma} \Vdash t': t \ep \intern{S}}{\Gamma \vdash t':t\ep S}

\infer{\Psi \Vdash t \ep U}{t \ep U \in \Psi }

&

\infer{\Psi \Vdash \lambda x.t\ep \Pi x:U. U'}
{\Psi, x \ep U \Vdash  t \ep U'}

\\
\\

\infer{\Psi \Vdash t\ep \Delta X^1. U}
{\Psi \Vdash t\ep U & X^1 \notin FV(\Psi)}

&
\infer{\Psi \Vdash  t\ep [U'/X] U}
{\Psi \Vdash t \ep \Delta X^1.U}

\\
\\
\infer{\Psi \Vdash  t_1 t_2 \ep [t_2/x]U}{\Psi
\Vdash  t_1 \ep \Pi x: U'.U & \Psi \Vdash  t_2 \ep U'}
\end{tabular}
}
\end{frame}

\begin{frame}
  \frametitle{Embedded to System $\mathfrak{G}$}

  $\interp{\cdot}$ is an \textbf{embedding} from internal types to sets, internal formula to formula.

  $\interp{X^1} := X^1$

  $\interp{\iota x.Q} := \iota x.\interp{Q}$

\yemph{$\interp{\Pi x:U'.U} := \iota f. \forall x. (x \ep \interp{U'} \to f\ x \ep \interp{U})$, where $f$ is fresh}.

\yemph{$\interp{\Delta X^1.U} := \iota x. (\Pi X^1. x \ep \interp{U})$, where $x$ is fresh}.

  $\interp{X^0} := X^0$

  $\interp{t\ep U} := t \ep \interp{U}$

  $\interp{Q \to Q'} := \interp{Q} \to \interp{Q}$

  $\interp{\Pi X^i.Q} := \Pi X^i.\interp{Q}$.

  $\interp{\forall x.Q} := \forall x.\interp{Q}$.

  $\interp{t\ep U, \Psi} :=  t\ep \interp{U}, \interp{\Psi}$



\end{frame}

\begin{frame}
  \frametitle{Reciprocity}
\begin{theorem}[Externalization, Meta]
\label{ext}
  If $\Psi \Vdash t \ep U$, then $\interp{\Psi} \vdash  t\ep \interp{U}$.
\end{theorem}

Let $\interp{\cdot}^{-1}$ be the inverse of $\interp{\cdot}$. 

\begin{definition}[Internalization]
  
\infer{\intern{\Gamma} \Vdash t \ep \intern{S}}{\Gamma \vdash t\ep S}    

\end{definition}
\end{frame}

\begin{frame}
\frametitle{Reasoning about Scott Numerals}
\begin{definition}[Scott numerals]
  \noindent $\mathsf{Nat} := \iota x. \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$

\noindent $\mathsf{S} \ := \lambda n. \lambda s.\lambda z. s \ n$

\noindent $0\  := \lambda s. \lambda z.z$

\end{definition}

\begin{theorem}
  $\cdot \vdash 0 \ep \mathsf{Nat}$.
\end{theorem}

\begin{proof}
  By comprehension, we want to show $\vdash \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to 0 \ep C$ \footnote{Note the proof terms for the theorem is Church numeral $0$.}. 
\end{proof}






\end{frame}

\begin{frame}
  \frametitle{Reasoning about Scott Numerals}
\begin{definition}[Scott numerals]
  \noindent $\mathsf{Nat} := \iota x. \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$
\end{definition}

  \begin{theorem}
$\cdot \vdash \forall m. (m \ep \mathsf{Nat} \to \mathsf{S}m \ep \mathsf{Nat})$.
\end{theorem}
  \begin{itemize}
  \item<1-> To show \yemph{$m \ep \mathsf{Nat} \vdash \mathsf{S}m \ep \mathsf{Nat} =_{\iota}$}
    
    \yemph{$ \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to \suc m \ep C$}. 
   \item<2->    By Intros, \yemph{$m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash \suc m \ep C$}. 

     \item<3-> We know \yemph{$m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash m \ep \mathsf{Nat} =_{\iota}$}

\yemph{$ \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to m \ep C$}
      \item<4-> By Modus Ponens, \yemph{$m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash m \ep C$}.

        \item<5-> We know \yemph{$m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash (m \ep C) \to (\mathsf{S} m)\ep C$}.

          \item<6-> Thus \yemph{$m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash \suc m \ep C$}\footnote{Note the proof terms for the theorem is Church successor.}. 

  \end{itemize}

\end{frame}

  \begin{frame}
      \frametitle{Reasoning about Scott Numerals}
    We just show $m \ep \mathsf{Nat} \vdash \mathsf{S}m \ep \mathsf{Nat}$. 
    \begin{itemize}
    \item<1->
          Internalization:
    
    $m \ep \intern{\mathsf{Nat}} \Vdash \mathsf{S}m \ep \intern{\mathsf{Nat}}$. 
    
    $\cdot \Vdash \lambda m.\mathsf{S}m \ep \Pi m: \nat. \mathsf{Nat}$
    \item<2->
          Externalization:
    
    $\cdot \vdash \lambda m.\mathsf{S}m \ep \interp{\Pi m: \nat. \mathsf{Nat}}$
    
    With $\interp{\Pi m: \nat. \mathsf{Nat}} = \iota f. \forall y.(y \ep \nat \to f\ y \ep \nat)$. 
%%    $\cdot \vdash \lambda m.\mathsf{S}m \ep \interp{\Pi m: \nat. \mathsf{Nat}} \equiv $
    
    $\cdot \vdash \lambda m.\mathsf{S}m \ep(\iota f. \forall y.(y \ep \nat \to f\ y \ep \nat)) =_{\iota,\beta}$
    
    $\cdot \vdash \forall y.(y \ep \nat \to \suc \ y \ep \nat)$

    \end{itemize}

    
  \end{frame}    

  \begin{frame}
          \frametitle{Reasoning about Scott Numerals}
  \begin{theorem}[Induction]
\

\noindent  $\cdot \vdash \Pi C^1. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$
\end{theorem}

  \begin{proof}
    \noindent Assuming $\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C, m \ep \mathsf{Nat}$, show $m \ep C$.
  \end{proof}
  \begin{definition}
  $\mathsf{add} :=  \lambda n. \lambda m.n\ (\lambda p. \mathsf{add}\ p\ (\mathsf{S} m))\ m$
\end{definition}
  
  \begin{theorem}
    $\cdot \vdash \forall m.\forall n. (m \ep \mathsf{Nat} \to n \ep \nat \to \add \ m \ n \ep \mathsf{Nat})$

    a.k.a. $\cdot \Vdash \add \ep \mathsf{Nat} \to \mathsf{Nat} \to \nat$
\end{theorem}
  \begin{proof}
    Use the induction theorem. 
  \end{proof}
  
    \end{frame}

  \begin{frame}
\frametitle{Pluralism}    
We define $x = y$ to be $\Pi C^1. x \ep C \to y \ep C$.

$\bot_0 := \Pi X^0.X$(basically unusable)

$\bot_1 := \forall x.\Pi X^1.x\ep X$(occasionally useful\footnote{e.g. prove empty set is a subset of any set})

$\bot_2 := \forall x.\forall y. x = y $(very useful)
  \begin{theorem}
         $\cdot \vdash \forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$.
  \end{theorem}
  Extend the notion of term reduction to include $\to_{\eta}, \to_{\Omega}$
  \begin{theorem}
    $\vdash \forall x. x\ep \nat \to ((x = \Omega) \to \bot_2)$
  \end{theorem}

  \begin{theorem}[Meta-level]
   System $\mathfrak{G}$ is consistent. The notion of Leibniz equality is faithful to the lambda term conversions. 
  \end{theorem}

  \end{frame}
  \begin{frame}
\frametitle{Summary}
\begin{itemize}
\item Introduce System $\mathfrak{G}$.
  \item A polymorphic depedent type system inside $\mathfrak{G}$.
 \item Potential to reason about program.
\end{itemize}
  \end{frame}



\begin{frame}
\frametitle{Thank you for listening!}

\begin{itemize}
\item Questions? 
\end{itemize}  
\end{frame}


\end{document}



